PERMUT.PRF[F82,JMC] - www.SailDart.org

perm filename PERMUT.PRF[F82,JMC] blob sn#688565 filedate 1982-11-22 generic text, type T, neo UTF8
(VERS3 0 (NIL ((SIMPINFO (#& . 0) (#& . 9) (#& . 16) (#& . 23) (#& . 28) (#& . 31) (#& . 32) (#& . 33) (#& . 34) (#& . 35) (#& . 36) (#& . 37) (#& . 38) (#& . 39) (#& . 40) (#& . 41) (#& . 42) (#& . 45) (#& . 46) (#& . 49) (#& . 50) (#& . 53) (#& . 54) (#& . 55) (#& . 56) (#& . 64) (#& . 67) (#& . 70) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 80)) (RCYCLEDEF (#& . 80)) (LCYCLEDEF (#& . 76)) (REVERSEAPPEND (#& . 86)) (REVERSEREVERSE (#& . 75)) (REVERSELIST (#& . 73)) (REVERSEDEF (#& . 70)) (REVPROP (#& . 87)) (REVDEF (#& . 67)) (REVERSEREV (#& . 72)) (SNOCDEF (#& . 78)) (RACDEF (#& . 88)) (RDCDEF (#& . 89)) (MEMBERDEF (#& . 90)) (ASSOCDEF (#& . 93)) (MKALIST (#& . 94)) (MAPCARDEF (#& . 95)) (SOMEPDEF (#& . 98)) (ALLPDEF (#& . 102)) (APPLASSOC (#& . 104)) (APPRASSOC (#& . 105)) (APPENDEF (#& . 53)) (LISTAPPEND (#& . 50)) (SEXPINDUCTIONDEF (#& . 106)) (SEXPINDUCTION (#& . 115)) (LISTINDUCTIONDEF (#& . 110)) (LISTINDUCTION (#& . 116))) ((CAR #& . 29) (CDR #& . 24) (ATOM #& . 1) (NULL #& . 26) (LISTP #& . 10) (ALISTP #& . 57) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (ZA #& . 5) (YA #& . 7) (XA #& . 8) (C #& . 117) (B #& . 119) (A #& . 120) (PHI #& . 99) (CONS #& . 21) (PARS #& . 107) (FUN #& . 109) (DEF #& . 111) (NILCASE #& . 112) (DEFSEXP #& . 113) (ATOMCASE #& . 114) (LIST #& . 43) (LST #& . 47) (APPEND #& . 51) (ALLP #& . 103) (SOMEP #& . 101) (MAPCAR #& . 96) (FN #& . 97) (A2 #& . 59) (A1 #& . 61) (A0 #& . 62) (ALIST #& . 63) (ASSOC #& . 65) (MEMBER #& . 91) (RAC #& . 81) (RDC #& . 83) (SNOC #& . 77) (REV #& . 68) (REVERSE #& . 71) (LCYCLE #& . 79) (RCYCLE #& . 85)) (PERMUT (#& . 82) (#& . 84) (#& . 121) (#& . 89) (#& . 88) (#& . 78) (#& . 123) (#& . 69) (#& . 72) (#& . 67) (#& . 87) (#& . 70) (#& . 73) (#& . 74) (#& . 75) (#& . 86) (#& . 125) (#& . 127) (#& . 76) (#& . 80)) (LISPAX (#& . 30) (#& . 25) (#& . 2) (#& . 27) (#& . 11) (#& . 58) (#& . 4) (#& . 13) (#& . 18) (#& . 6) (#& . 118) (#& . 100) (#& . 22) (#& . 0) (#& . 9) (#& . 16) (#& . 23) (#& . 28) (#& . 31) (#& . 32) (#& . 33) (#& . 34) (#& . 35) (#& . 36) (#& . 37) (#& . 38) (#& . 39) (#& . 40) (#& . 41) (#& . 116) (#& . 108) (#& . 110) (#& . 115) (#& . 106) (#& . 44) (#& . 48) (#& . 42) (#& . 45) (#& . 46) (#& . 49) (#& . 52) (#& . 50) (#& . 53) (#& . 54) (#& . 55) (#& . 105) (#& . 104) (#& . 102) (#& . 98) (#& . 95) (#& . 60) (#& . 56) (#& . 129) (#& . 94) (#& . 66) (#& . 93) (#& . 64) (#& . 92) (#& . 90))) ((((∀ ALIST)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . ALIST))) ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ATOM) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . ALIST)))) ((SYMBOL& NIL . ATOM) NIL ((SYMBOL& NIL . CAR) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . ALIST))))))) . (AXIOM (TM& ((∀ ALIST)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . ALIST))) ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ATOM) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . ALIST)))) ((SYMBOL& NIL . ATOM) NIL ((SYMBOL& NIL . CAR) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . ALIST)))))))) . ((CAR #& . 29) (ATOM #& . 1) (NULL #& . 26) (ALISTP #& . 57) (A2 #& . 59) (A1 #& . 61) (A0 #& . 62) (ALIST #& . 63)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 53 .) ((→ GROUND GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 950) (UNARY& . RCYCLE)) . (#& . 127) . CONSTANT .) (NIL . (DECL RCYCLE (UNARYNAME: RCYCLE) (TYPE: (TY& → GROUND GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((RCYCLE #& . 128)) . NIL . NIL . NIL . PERMUT . NIL . 18 .) ((→ GROUND GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 950) (UNARY& . LCYCLE)) . (#& . 125) . CONSTANT .) (NIL . (DECL LCYCLE (UNARYNAME: LCYCLE) (TYPE: (TY& → GROUND GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((LCYCLE #& . 126)) . NIL . NIL . NIL . PERMUT . NIL . 17 .) ((→ GROUND GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 950) (UNARY& . REVERSE)) . (#& . 123) . CONSTANT .) (NIL . (DECL REVERSE (UNARYNAME: REVERSE) (TYPE: (TY& → GROUND GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((REVERSE #& . 124)) . NIL . NIL . NIL . PERMUT . NIL . 7 .) ((→ (⊗ GROUND GROUND) GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 121) . CONSTANT .) (NIL . (DECL SNOC (TYPE: (TY& → (⊗ GROUND GROUND) GROUND)) (SYNTYPE: CONSTANT)) . ((SNOC #& . 122)) . NIL . NIL . NIL . PERMUT . NIL . 3 .) (GROUND . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 118) . VARIABLE .) (GROUND . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 118) . VARIABLE .) (NIL . (DECL (A B C) (TYPE: (TY& . GROUND))) . ((C #& . 117) (B #& . 119) (A #& . 120)) . NIL . NIL . NIL . LISPAX . NIL . 11 .) (GROUND . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 118) . VARIABLE .) ((((∀ PHI)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . PHI) NIL (META& NIL)) (((∀ X U)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . U)) ((SYMBOL& NIL . PHI) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)))))) (((∀ U)) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . U))))) . (AXIOM (TM& ((∀ PHI)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . PHI) NIL (META& NIL)) (((∀ X U)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . U)) ((SYMBOL& NIL . PHI) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)))))) (((∀ U)) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . U)))))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (PHI #& . 99) (CONS #& . 21)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 30 .) ((((∀ PHI)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ∧) NIL (((∀ X)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ATOM) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . X)))) (((∀ X Y)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . Y))) ((SYMBOL& NIL . PHI) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y)))))) (((∀ X)) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . X))))) . (AXIOM (TM& ((∀ PHI)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ∧) NIL (((∀ X)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ATOM) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . X)))) (((∀ X Y)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . Y))) ((SYMBOL& NIL . PHI) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y)))))) (((∀ X)) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . X)))))) . ((ATOM #& . 1) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (PHI #& . 99) (CONS #& . 21)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 33 .) ((→ (⊗ GROUND (* GROUND)) GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 106) . VARIABLE .) ((→ (⊗ GROUND GROUND GROUND GROUND (* GROUND)) GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 106) . VARIABLE .) ((→ (* GROUND) GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 110) . VARIABLE .) ((→ (⊗ GROUND GROUND GROUND (* GROUND)) GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 110) . VARIABLE .) ((((∀ NILCASE DEF)) NIL (((∃ FUN)) NIL (((∀ PARS X U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . FUN) NIL (META& NIL) (SYMBOL& NIL . PARS)) ((SYMBOL& NIL . NILCASE) NIL (SYMBOL& NIL . PARS))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . FUN) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)) (SYMBOL& NIL . PARS)) ((SYMBOL& NIL . DEF) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U) ((SYMBOL& NIL . FUN) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . PARS)) (SYMBOL& NIL . PARS))))))) . (AXIOM (TM& ((∀ NILCASE DEF)) NIL (((∃ FUN)) NIL (((∀ PARS X U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . FUN) NIL (META& NIL) (SYMBOL& NIL . PARS)) ((SYMBOL& NIL . NILCASE) NIL (SYMBOL& NIL . PARS))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . FUN) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)) (SYMBOL& NIL . PARS)) ((SYMBOL& NIL . DEF) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U) ((SYMBOL& NIL . FUN) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . PARS)) (SYMBOL& NIL . PARS)))))))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (PARS #& . 107) (FUN #& . 109) (DEF #& . 111) (NILCASE #& . 112)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 32 .) ((→ (⊗ GROUND (* GROUND)) GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 110) . VARIABLE .) (NIL . (DECL PARS (TYPE: (TY& * GROUND))) . ((PARS #& . 107)) . NIL . NIL . NIL . LISPAX . NIL . 31 .) ((* GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 108) . VARIABLE .) ((((∀ ATOMCASE DEFSEXP)) NIL (((∃ FUN)) NIL (((∀ PARS X Y)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ATOM) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . FUN) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . PARS)) ((SYMBOL& NIL . ATOMCASE) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . PARS)))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . FUN) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y)) (SYMBOL& NIL . PARS)) ((SYMBOL& NIL . DEFSEXP) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y) ((SYMBOL& NIL . FUN) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . PARS)) ((SYMBOL& NIL . FUN) NIL (SYMBOL& NIL . Y) (SYMBOL& NIL . PARS)) (SYMBOL& NIL . PARS))))))) . (AXIOM (TM& ((∀ ATOMCASE DEFSEXP)) NIL (((∃ FUN)) NIL (((∀ PARS X Y)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ATOM) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . FUN) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . PARS)) ((SYMBOL& NIL . ATOMCASE) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . PARS)))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . FUN) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y)) (SYMBOL& NIL . PARS)) ((SYMBOL& NIL . DEFSEXP) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y) ((SYMBOL& NIL . FUN) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . PARS)) ((SYMBOL& NIL . FUN) NIL (SYMBOL& NIL . Y) (SYMBOL& NIL . PARS)) (SYMBOL& NIL . PARS)))))))) . ((ATOM #& . 1) (LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (PARS #& . 107) (FUN #& . 109) (DEF #& . 111) (NILCASE #& . 112) (DEFSEXP #& . 113) (ATOMCASE #& . 114)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 34 .) ((((∀ U V W)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V) (SYMBOL& NIL . W)) ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . V) (SYMBOL& NIL . W))))) . (AXIOM (TM& ((∀ U V W)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V) (SYMBOL& NIL . W)) ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . V) (SYMBOL& NIL . W)))))) . ((LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15) (APPEND #& . 51)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 46 .) ((((∀ U V W)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V) (SYMBOL& NIL . W)) ((SYMBOL& NIL . APPEND) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V)) (SYMBOL& NIL . W)))) . (AXIOM (TM& ((∀ U V W)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V) (SYMBOL& NIL . W)) ((SYMBOL& NIL . APPEND) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V)) (SYMBOL& NIL . W))))) . ((LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15) (APPEND #& . 51)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 47 .) ((→ (⊗ (→ GROUND TRUTHVAL) GROUND) TRUTHVAL) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 102) . VARIABLE .) ((((∀ PHI X U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . ALLP) NIL (SYMBOL& NIL . PHI) (META& NIL)) ((SYMBOL& NIL . CONDI) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . ALLP) NIL (SYMBOL& NIL . PHI) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . ALLP) NIL (SYMBOL& NIL . PHI) (SYMBOL& NIL . U))) ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ALLP) NIL (SYMBOL& NIL . PHI) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))))))) . (AXIOM (TM& ((∀ PHI X U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . ALLP) NIL (SYMBOL& NIL . PHI) (META& NIL)) ((SYMBOL& NIL . CONDI) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . ALLP) NIL (SYMBOL& NIL . PHI) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . ALLP) NIL (SYMBOL& NIL . PHI) (SYMBOL& NIL . U))) ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ALLP) NIL (SYMBOL& NIL . PHI) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)))))))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (PHI #& . 99) (CONS #& . 21) (ALLP #& . 103)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 48 .) ((→ (⊗ (→ GROUND TRUTHVAL) GROUND) TRUTHVAL) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 98) . VARIABLE .) (NIL . (DECL (PHI) (TYPE: (TY& → GROUND TRUTHVAL))) . ((PHI #& . 99)) . NIL . NIL . NIL . LISPAX . NIL . 12 .) ((→ GROUND TRUTHVAL) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 100) . VARIABLE .) ((((∀ PHI X U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . SOMEP) NIL (SYMBOL& NIL . PHI) (META& NIL))) ((SYMBOL& NIL . CONDI) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . SOMEP) NIL (SYMBOL& NIL . PHI) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . SOMEP) NIL (SYMBOL& NIL . PHI) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . SOMEP) NIL (SYMBOL& NIL . PHI) (SYMBOL& NIL . U)))))) . (AXIOM (TM& ((∀ PHI X U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . SOMEP) NIL (SYMBOL& NIL . PHI) (META& NIL))) ((SYMBOL& NIL . CONDI) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . SOMEP) NIL (SYMBOL& NIL . PHI) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . SOMEP) NIL (SYMBOL& NIL . PHI) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . SOMEP) NIL (SYMBOL& NIL . PHI) (SYMBOL& NIL . U))))))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (PHI #& . 99) (CONS #& . 21) (SOMEP #& . 101)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 49 .) ((→ GROUND GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 95) . VARIABLE .) ((→ (⊗ (→ GROUND GROUND) GROUND) GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 95) . VARIABLE .) ((((∀ FN X U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . MAPCAR) NIL (SYMBOL& NIL . FN) (META& NIL)) (META& NIL)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . MAPCAR) NIL (SYMBOL& NIL . FN) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . FN) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . MAPCAR) NIL (SYMBOL& NIL . FN) (SYMBOL& NIL . U)))))) . (AXIOM (TM& ((∀ FN X U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . MAPCAR) NIL (SYMBOL& NIL . FN) (META& NIL)) (META& NIL)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . MAPCAR) NIL (SYMBOL& NIL . FN) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . FN) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . MAPCAR) NIL (SYMBOL& NIL . FN) (SYMBOL& NIL . U))))))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (MAPCAR #& . 96) (FN #& . 97)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 50 .) ((((∀ XA Y ALIST)) NIL ((SYMBOL& NIL . ALISTP) NIL ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . XA) (SYMBOL& NIL . Y)) (SYMBOL& NIL . ALIST)))) . (AXIOM (TM& ((∀ XA Y ALIST)) NIL ((SYMBOL& NIL . ALISTP) NIL ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . XA) (SYMBOL& NIL . Y)) (SYMBOL& NIL . ALIST))))) . ((ATOM #& . 1) (ALISTP #& . 57) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (ZA #& . 5) (YA #& . 7) (XA #& . 8) (CONS #& . 21) (A2 #& . 59) (A1 #& . 61) (A0 #& . 62) (ALIST #& . 63)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 54 .) ((((∀ X XA Y ALIST)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . ASSOC) NIL (SYMBOL& NIL . X) (META& NIL)) (META& NIL)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . ASSOC) NIL (SYMBOL& NIL . X) ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . XA) (SYMBOL& NIL . Y)) (SYMBOL& NIL . ALIST))) ((SYMBOL& NIL . CONDI) NIL ((SYMBOL& NIL . =) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . XA)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . XA) (SYMBOL& NIL . Y)) ((SYMBOL& NIL . ASSOC) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . ALIST)))))) . (AXIOM (TM& ((∀ X XA Y ALIST)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . ASSOC) NIL (SYMBOL& NIL . X) (META& NIL)) (META& NIL)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . ASSOC) NIL (SYMBOL& NIL . X) ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . XA) (SYMBOL& NIL . Y)) (SYMBOL& NIL . ALIST))) ((SYMBOL& NIL . CONDI) NIL ((SYMBOL& NIL . =) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . XA)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . XA) (SYMBOL& NIL . Y)) ((SYMBOL& NIL . ASSOC) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . ALIST))))))) . ((ATOM #& . 1) (ALISTP #& . 57) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (ZA #& . 5) (YA #& . 7) (XA #& . 8) (CONS #& . 21) (A2 #& . 59) (A1 #& . 61) (A0 #& . 62) (ALIST #& . 63) (ASSOC #& . 65)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 56 .) (NIL . (DECL MEMBER (TYPE: (TY& → (⊗ GROUND GROUND) TRUTHVAL)) (SYNTYPE: CONSTANT)) . ((MEMBER #& . 91)) . NIL . NIL . NIL . LISPAX . NIL . 58 .) ((→ (⊗ GROUND GROUND) TRUTHVAL) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 92) . CONSTANT .) ((((∀ X Y U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . MEMBER) NIL (SYMBOL& NIL . X) (META& NIL))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . MEMBER) NIL (SYMBOL& NIL . X) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . Y) (SYMBOL& NIL . U))) ((SYMBOL& NIL . ∨) NIL ((SYMBOL& NIL . =) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y)) ((SYMBOL& NIL . MEMBER) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)))))) . (AXIOM (TM& ((∀ X Y U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . MEMBER) NIL (SYMBOL& NIL . X) (META& NIL))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . MEMBER) NIL (SYMBOL& NIL . X) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . Y) (SYMBOL& NIL . U))) ((SYMBOL& NIL . ∨) NIL ((SYMBOL& NIL . =) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y)) ((SYMBOL& NIL . MEMBER) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))))))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (MEMBER #& . 91)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 59 .) ((((∀ X U)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . RDC) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . CONDI) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U)) (META& NIL) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) ((SYMBOL& NIL . RDC) NIL (SYMBOL& NIL . U)))))) . (AXIOM (TM& ((∀ X U)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . RDC) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . CONDI) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U)) (META& NIL) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) ((SYMBOL& NIL . RDC) NIL (SYMBOL& NIL . U))))))) . ((NULL #& . 26) (LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (RDC #& . 83)) . NIL . ((&& . 1)) . NIL . PERMUT . NIL . 4 .) ((((∀ X U)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . RAC) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . CONDI) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U)) (SYMBOL& NIL . X) ((SYMBOL& NIL . RAC) NIL (SYMBOL& NIL . U))))) . (AXIOM (TM& ((∀ X U)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . RAC) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . CONDI) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U)) (SYMBOL& NIL . X) ((SYMBOL& NIL . RAC) NIL (SYMBOL& NIL . U)))))) . ((NULL #& . 26) (LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (RAC #& . 81)) . NIL . ((&& . 1)) . NIL . PERMUT . NIL . 5 .) ((((∀ U V)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . REV) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V)) ((SYMBOL& NIL . APPEND) NIL ((SYMBOL& NIL . REVERSE) NIL (SYMBOL& NIL . U)) (SYMBOL& NIL . V)))) . (AXIOM (TM& ((∀ U V)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . REV) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V)) ((SYMBOL& NIL . APPEND) NIL ((SYMBOL& NIL . REVERSE) NIL (SYMBOL& NIL . U)) (SYMBOL& NIL . V))))) . ((LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15) (APPEND #& . 51) (REV #& . 68) (REVERSE #& . 71)) . NIL . ((&& . 1)) . NIL . PERMUT . NIL . 11 .) ((((∀ U V)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . REVERSE) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V))) ((SYMBOL& NIL . APPEND) NIL ((SYMBOL& NIL . REVERSE) NIL (SYMBOL& NIL . V)) ((SYMBOL& NIL . REVERSE) NIL (SYMBOL& NIL . U))))) . (AXIOM (TM& ((∀ U V)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . REVERSE) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V))) ((SYMBOL& NIL . APPEND) NIL ((SYMBOL& NIL . REVERSE) NIL (SYMBOL& NIL . V)) ((SYMBOL& NIL . REVERSE) NIL (SYMBOL& NIL . U)))))) . ((LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15) (APPEND #& . 51) (REV #& . 68) (REVERSE #& . 71)) . NIL . ((&& . 1)) . NIL . PERMUT . NIL . 16 .) ((→ GROUND GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 950) (UNARY& . RCYCLE)) . (#& . 80) . DEFINED .) (NIL . (DECL RDC (UNARYNAME: RDC) (TYPE: (TY& → GROUND GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((RDC #& . 83)) . NIL . NIL . NIL . PERMUT . NIL . 2 .) ((→ GROUND GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 950) (UNARY& . RDC)) . (#& . 84) . CONSTANT .) (NIL . (DECL RAC (UNARYNAME: RAC) (TYPE: (TY& → GROUND GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((RAC #& . 81)) . NIL . NIL . NIL . PERMUT . NIL . 1 .) ((→ GROUND GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 950) (UNARY& . RAC)) . (#& . 82) . CONSTANT .) ((((∀ U)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . RCYCLE) NIL (SYMBOL& NIL . U)) ((SYMBOL& NIL . CONDI) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U)) (META& NIL) ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . RAC) NIL (SYMBOL& NIL . U)) ((SYMBOL& NIL . RDC) NIL (SYMBOL& NIL . U)))))) . (DEFINE RCYCLE (TM& ((∀ U)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . RCYCLE) NIL (SYMBOL& NIL . U)) ((SYMBOL& NIL . CONDI) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U)) (META& NIL) ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . RAC) NIL (SYMBOL& NIL . U)) ((SYMBOL& NIL . RDC) NIL (SYMBOL& NIL . U)))))) NIL) . ((NULL #& . 26) (LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15) (CONS #& . 21) (RAC #& . 81) (RDC #& . 83) (RCYCLE #& . 85)) . NIL . ((&& . 1)) . NIL . PERMUT . NIL . 20 .) ((→ GROUND GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 950) (UNARY& . LCYCLE)) . (#& . 76) . DEFINED .) ((((∀ X U)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . SNOC) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)) ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (META& NIL))))) . (DEFINE SNOC (TM& ((∀ X U)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . SNOC) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)) ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (META& NIL))))) NIL) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (APPEND #& . 51) (SNOC #& . 77)) . NIL . ((&& . 1)) . NIL . PERMUT . NIL . 6 .) ((→ (⊗ GROUND GROUND) GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 78) . DEFINED .) ((((∀ U)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . LCYCLE) NIL (SYMBOL& NIL . U)) ((SYMBOL& NIL . CONDI) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U)) (META& NIL) ((SYMBOL& NIL . SNOC) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . U)) ((SYMBOL& NIL . CDR) NIL (SYMBOL& NIL . U)))))) . (DEFINE LCYCLE (TM& ((∀ U)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . LCYCLE) NIL (SYMBOL& NIL . U)) ((SYMBOL& NIL . CONDI) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U)) (META& NIL) ((SYMBOL& NIL . SNOC) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . U)) ((SYMBOL& NIL . CDR) NIL (SYMBOL& NIL . U)))))) NIL) . ((CAR #& . 29) (CDR #& . 24) (NULL #& . 26) (LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (APPEND #& . 51) (SNOC #& . 77) (LCYCLE #& . 79)) . NIL . ((&& . 1)) . NIL . PERMUT . NIL . 19 .) ((((∀ U)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . REVERSE) NIL ((SYMBOL& NIL . REVERSE) NIL (SYMBOL& NIL . U))) (SYMBOL& NIL . U))) . (AXIOM (TM& ((∀ U)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . REVERSE) NIL ((SYMBOL& NIL . REVERSE) NIL (SYMBOL& NIL . U))) (SYMBOL& NIL . U)))) . ((LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15) (REV #& . 68) (REVERSE #& . 71)) . NIL . ((&& . 1)) . NIL . PERMUT . NIL . 15 .) ((((∀ X)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . REVERSE) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (META& NIL))) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (META& NIL)))) . (AXIOM (TM& ((∀ X)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . REVERSE) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (META& NIL))) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (META& NIL))))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (REV #& . 68) (REVERSE #& . 71)) . NIL . ((&& . 1)) . NIL . PERMUT . NIL . 14 .) ((((∀ U)) NIL ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . REVERSE) NIL (SYMBOL& NIL . U)))) . (AXIOM (TM& ((∀ U)) NIL ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . REVERSE) NIL (SYMBOL& NIL . U))))) . ((LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15) (REV #& . 68) (REVERSE #& . 71)) . NIL . ((&& . 1)) . NIL . PERMUT . NIL . 13 .) ((((∀ U)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . REVERSE) NIL (SYMBOL& NIL . U)) ((SYMBOL& NIL . REV) NIL (SYMBOL& NIL . U) (META& NIL)))) . (DEFINE REVERSE (TM& ((∀ U)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . REVERSE) NIL (SYMBOL& NIL . U)) ((SYMBOL& NIL . REV) NIL (SYMBOL& NIL . U) (META& NIL)))) NIL) . ((LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15) (REV #& . 68) (REVERSE #& . 71)) . NIL . ((&& . 1)) . NIL . PERMUT . NIL . 9 .) ((→ GROUND GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 950) (UNARY& . REVERSE)) . (#& . 72) . DEFINED .) ((((∀ X U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . REVERSE) NIL (META& NIL)) (META& NIL)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . REVERSE) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . APPEND) NIL ((SYMBOL& NIL . REVERSE) NIL (SYMBOL& NIL . U)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (META& NIL)))))) . (AXIOM (TM& ((∀ X U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . REVERSE) NIL (META& NIL)) (META& NIL)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . REVERSE) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . APPEND) NIL ((SYMBOL& NIL . REVERSE) NIL (SYMBOL& NIL . U)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (META& NIL))))))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (APPEND #& . 51) (REV #& . 68) (REVERSE #& . 71)) . NIL . ((&& . 1)) . NIL . PERMUT . NIL . 12 .) (NIL . (DECL REV (TYPE: (TY& → (⊗ GROUND GROUND) GROUND)) (SYNTYPE: CONSTANT)) . ((REV #& . 68)) . NIL . NIL . NIL . PERMUT . NIL . 8 .) ((→ (⊗ GROUND GROUND) GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 69) . CONSTANT .) ((((∀ X U V)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . REV) NIL (META& NIL) (SYMBOL& NIL . V)) (SYMBOL& NIL . V)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . REV) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)) (SYMBOL& NIL . V)) ((SYMBOL& NIL . REV) NIL (SYMBOL& NIL . U) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . V)))))) . (AXIOM (TM& ((∀ X U V)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . REV) NIL (META& NIL) (SYMBOL& NIL . V)) (SYMBOL& NIL . V)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . REV) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)) (SYMBOL& NIL . V)) ((SYMBOL& NIL . REV) NIL (SYMBOL& NIL . U) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . V))))))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (REV #& . 68)) . NIL . ((&& . 1)) . NIL . PERMUT . NIL . 10 .) (NIL . (DECL ASSOC (TYPE: (TY& → (⊗ GROUND GROUND) GROUND)) (SYNTYPE: CONSTANT)) . ((ASSOC #& . 65)) . NIL . NIL . NIL . LISPAX . NIL . 55 .) ((→ (⊗ GROUND GROUND) GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 66) . CONSTANT .) ((((∀ X ALIST)) NIL ((SYMBOL& NIL . SEXP) NIL ((SYMBOL& NIL . ASSOC) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . ALIST)))) . (AXIOM (TM& ((∀ X ALIST)) NIL ((SYMBOL& NIL . SEXP) NIL ((SYMBOL& NIL . ASSOC) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . ALIST))))) . ((ALISTP #& . 57) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (A2 #& . 59) (A1 #& . 61) (A0 #& . 62) (ALIST #& . 63) (ASSOC #& . 65)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 57 .) (GROUND . (SYMBOL& NIL . ALISTP) . NIL . NIL . (#& . 60) . VARIABLE .) (GROUND . (SYMBOL& NIL . ALISTP) . NIL . NIL . (#& . 60) . VARIABLE .) (GROUND . (SYMBOL& NIL . ALISTP) . NIL . NIL . (#& . 60) . VARIABLE .) (NIL . (DECL (ALIST A0 A1 A2) (TYPE: (TY& . GROUND)) (SORT: (TM& SYMBOL& NIL . ALISTP))) . ((A2 #& . 59) (ALISTP #& . 57) (A1 #& . 61) (ALISTP #& . 57) (A0 #& . 62) (ALISTP #& . 57) (ALIST #& . 63) (ALISTP #& . 57)) . NIL . NIL . NIL . LISPAX . NIL . 51 .) (GROUND . (SYMBOL& NIL . ALISTP) . NIL . NIL . (#& . 60) . VARIABLE .) (NIL . (DECL ALISTP (UNARYNAME: ALISTP) (TYPE: (TY& → GROUND TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((ALISTP #& . 57)) . NIL . NIL . NIL . LISPAX . NIL . 6 .) ((→ GROUND TRUTHVAL) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 750) (UNARY& . ALISTP)) . (#& . 58) . CONSTANT .) ((((∀ ALIST)) NIL ((SYMBOL& NIL . LISTP) NIL (SYMBOL& NIL . ALIST))) . (AXIOM (TM& ((∀ ALIST)) NIL ((SYMBOL& NIL . LISTP) NIL (SYMBOL& NIL . ALIST)))) . ((LISTP #& . 10) (ALISTP #& . 57) (A2 #& . 59) (A1 #& . 61) (A0 #& . 62) (ALIST #& . 63)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 52 .) ((((∀ X V)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (META& NIL)) (SYMBOL& NIL . V)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . V)))) . (AXIOM (TM& ((∀ X V)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (META& NIL)) (SYMBOL& NIL . V)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . V))))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (APPEND #& . 51)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 45 .) ((((∀ U)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (META& NIL)) (SYMBOL& NIL . U))) . (AXIOM (TM& ((∀ U)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (META& NIL)) (SYMBOL& NIL . U)))) . ((LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15) (APPEND #& . 51)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 44 .) ((((∀ X U V)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL (META& NIL) (SYMBOL& NIL . V)) (SYMBOL& NIL . V)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)) (SYMBOL& NIL . V)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V)))))) . (AXIOM (TM& ((∀ X U V)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL (META& NIL) (SYMBOL& NIL . V)) (SYMBOL& NIL . V)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)) (SYMBOL& NIL . V)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V))))))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (APPEND #& . 51)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 43 .) (NIL . (DECL APPEND (TYPE: (TY& → (⊗ GROUND (* GROUND)) GROUND)) (SYNTYPE: CONSTANT) (ASSOCIATIVITY: BOTH) (INFIXNAME: *) (BINDINGPOWER: 840)) . ((APPEND #& . 51)) . NIL . NIL . NIL . LISPAX . NIL . 41 .) ((→ (⊗ GROUND (* GROUND)) GROUND) . (SYMBOL& NIL . UNIVERSAL) . BOTH . ((BINDP& . 840) (INFIX& . *)) . (#& . 52) . CONSTANT .) ((((∀ U V)) NIL ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V)))) . (AXIOM (TM& ((∀ U V)) NIL ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V))))) . ((LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15) (APPEND #& . 51)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 42 .) ((((∀ X LST)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . LIST) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . LST)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) ((SYMBOL& NIL . LIST) NIL (SYMBOL& NIL . LST))))) . (AXIOM (TM& ((∀ X LST)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . LIST) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . LST)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) ((SYMBOL& NIL . LIST) NIL (SYMBOL& NIL . LST)))))) . ((SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (LIST #& . 43) (LST #& . 47)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 40 .) (NIL . (DECL LST (TYPE: (TY& * GROUND))) . ((LST #& . 47)) . NIL . NIL . NIL . LISPAX . NIL . 36 .) ((* GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 48) . VARIABLE .) ((((∀ LST)) NIL ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . LIST) NIL (SYMBOL& NIL . LST)))) . (AXIOM (TM& ((∀ LST)) NIL ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . LIST) NIL (SYMBOL& NIL . LST))))) . ((LISTP #& . 10) (LIST #& . 43) (LST #& . 47)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 39 .) ((((∀ X)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . LIST) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (META& NIL)))) . (AXIOM (TM& ((∀ X)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . LIST) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (META& NIL))))) . ((SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (LIST #& . 43)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 38 .) (NIL . (DECL LIST (TYPE: (TY& → (* GROUND) GROUND)) (SYNTYPE: CONSTANT)) . ((LIST #& . 43)) . NIL . NIL . NIL . LISPAX . NIL . 35 .) ((→ (* GROUND) GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 44) . CONSTANT .) ((((∀ X)) NIL ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . LIST) NIL (SYMBOL& NIL . X)))) . (AXIOM (TM& ((∀ X)) NIL ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . LIST) NIL (SYMBOL& NIL . X))))) . ((LISTP #& . 10) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (LIST #& . 43)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 37 .) ((((∀ X)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ATOM) NIL (SYMBOL& NIL . X))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . CDR) NIL (SYMBOL& NIL . X))) (SYMBOL& NIL . X)))) . (AXIOM (TM& ((∀ X)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ATOM) NIL (SYMBOL& NIL . X))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . CDR) NIL (SYMBOL& NIL . X))) (SYMBOL& NIL . X))))) . ((CAR #& . 29) (CDR #& . 24) (ATOM #& . 1) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 29 .) ((((∀ U)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . U)) ((SYMBOL& NIL . CDR) NIL (SYMBOL& NIL . U))) (SYMBOL& NIL . U)))) . (AXIOM (TM& ((∀ U)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . U)) ((SYMBOL& NIL . CDR) NIL (SYMBOL& NIL . U))) (SYMBOL& NIL . U))))) . ((CAR #& . 29) (CDR #& . 24) (NULL #& . 26) (LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15) (CONS #& . 21)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 28 .) ((((∀ X Y)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . CDR) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y))) (SYMBOL& NIL . Y))) . (AXIOM (TM& ((∀ X Y)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . CDR) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y))) (SYMBOL& NIL . Y)))) . ((CDR #& . 24) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 27 .) ((((∀ X Y)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . CAR) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y))) (SYMBOL& NIL . X))) . (AXIOM (TM& ((∀ X Y)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . CAR) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y))) (SYMBOL& NIL . X)))) . ((CAR #& . 29) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 26 .) ((((∀ X U)) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . NULL) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))))) . (AXIOM (TM& ((∀ X U)) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . NULL) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)))))) . ((NULL #& . 26) (LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 25 .) ((((∀ X Y)) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ATOM) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y))))) . (AXIOM (TM& ((∀ X Y)) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ATOM) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y)))))) . ((ATOM #& . 1) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 24 .) ((((∀ X Y)) NIL ((SYMBOL& NIL . SEXP) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y)))) . (AXIOM (TM& ((∀ X Y)) NIL ((SYMBOL& NIL . SEXP) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y))))) . ((SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 23 .) ((((∀ U)) NIL ((SYMBOL& NIL . ≡) NIL ((SYMBOL& NIL . =) NIL (META& NIL) (SYMBOL& NIL . U)) ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U)))) . (AXIOM (TM& ((∀ U)) NIL ((SYMBOL& NIL . ≡) NIL ((SYMBOL& NIL . =) NIL (META& NIL) (SYMBOL& NIL . U)) ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U))))) . ((NULL #& . 26) (LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 22 .) ((((∀ U)) NIL ((SYMBOL& NIL . ≡) NIL ((SYMBOL& NIL . =) NIL (SYMBOL& NIL . U) (META& NIL)) ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U)))) . (AXIOM (TM& ((∀ U)) NIL ((SYMBOL& NIL . ≡) NIL ((SYMBOL& NIL . =) NIL (SYMBOL& NIL . U) (META& NIL)) ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U))))) . ((NULL #& . 26) (LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 21 .) ((((∀ X)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ATOM) NIL (SYMBOL& NIL . X))) ((SYMBOL& NIL . SEXP) NIL ((SYMBOL& NIL . CDR) NIL (SYMBOL& NIL . X))))) . (AXIOM (TM& ((∀ X)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ATOM) NIL (SYMBOL& NIL . X))) ((SYMBOL& NIL . SEXP) NIL ((SYMBOL& NIL . CDR) NIL (SYMBOL& NIL . X)))))) . ((CDR #& . 24) (ATOM #& . 1) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 20 .) ((((∀ X)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ATOM) NIL (SYMBOL& NIL . X))) ((SYMBOL& NIL . SEXP) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . X))))) . (AXIOM (TM& ((∀ X)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ATOM) NIL (SYMBOL& NIL . X))) ((SYMBOL& NIL . SEXP) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . X)))))) . ((CAR #& . 29) (ATOM #& . 1) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 19 .) (NIL . (DECL CAR (UNARYNAME: CAR) (TYPE: (TY& → GROUND GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((CAR #& . 29)) . NIL . NIL . NIL . LISPAX . NIL . 1 .) ((→ GROUND GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 950) (UNARY& . CAR)) . (#& . 30) . CONSTANT .) ((((∀ U)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U))) ((SYMBOL& NIL . SEXP) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . U))))) . (AXIOM (TM& ((∀ U)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U))) ((SYMBOL& NIL . SEXP) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . U)))))) . ((CAR #& . 29) (NULL #& . 26) (LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 18 .) (NIL . (DECL NULL (UNARYNAME: NULL) (TYPE: (TY& → GROUND TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((NULL #& . 26)) . NIL . NIL . NIL . LISPAX . NIL . 4 .) ((→ GROUND TRUTHVAL) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 750) (UNARY& . NULL)) . (#& . 27) . CONSTANT .) (NIL . (DECL CDR (UNARYNAME: CDR) (TYPE: (TY& → GROUND GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((CDR #& . 24)) . NIL . NIL . NIL . LISPAX . NIL . 2 .) ((→ GROUND GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 950) (UNARY& . CDR)) . (#& . 25) . CONSTANT .) ((((∀ U)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U))) ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . CDR) NIL (SYMBOL& NIL . U))))) . (AXIOM (TM& ((∀ U)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U))) ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . CDR) NIL (SYMBOL& NIL . U)))))) . ((CDR #& . 24) (NULL #& . 26) (LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 17 .) (NIL . (DECL CONS (TYPE: (TY& → (⊗ GROUND GROUND) GROUND)) (SYNTYPE: CONSTANT) (INFIXNAME: |.|) (PREFIXNAME: CONS) (BINDINGPOWER: 850)) . ((CONS #& . 21)) . NIL . NIL . NIL . LISPAX . NIL . 13 .) ((→ (⊗ GROUND GROUND) GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 850) (PREFIX& . CONS) (INFIX& . |.|)) . (#& . 22) . CONSTANT .) (GROUND . (SYMBOL& NIL . SEXP) . NIL . NIL . (#& . 18) . VARIABLE .) (GROUND . (SYMBOL& NIL . SEXP) . NIL . NIL . (#& . 18) . VARIABLE .) (NIL . (DECL (X Y Z) (TYPE: (TY& . GROUND)) (SORT: (TM& SYMBOL& NIL . SEXP))) . ((Z #& . 17) (SEXP #& . 3) (Y #& . 19) (SEXP #& . 3) (X #& . 20) (SEXP #& . 3)) . NIL . NIL . NIL . LISPAX . NIL . 9 .) (GROUND . (SYMBOL& NIL . SEXP) . NIL . NIL . (#& . 18) . VARIABLE .) ((((∀ X U)) NIL ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)))) . (AXIOM (TM& ((∀ X U)) NIL ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 16 .) (GROUND . (SYMBOL& NIL . LISTP) . NIL . NIL . (#& . 13) . VARIABLE .) (GROUND . (SYMBOL& NIL . LISTP) . NIL . NIL . (#& . 13) . VARIABLE .) (NIL . (DECL (U V W) (TYPE: (TY& . GROUND)) (SORT: (TM& SYMBOL& NIL . LISTP))) . ((W #& . 12) (LISTP #& . 10) (V #& . 14) (LISTP #& . 10) (U #& . 15) (LISTP #& . 10)) . NIL . NIL . NIL . LISPAX . NIL . 8 .) (GROUND . (SYMBOL& NIL . LISTP) . NIL . NIL . (#& . 13) . VARIABLE .) (NIL . (DECL LISTP (UNARYNAME: LISTP) (TYPE: (TY& → GROUND TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((LISTP #& . 10)) . NIL . NIL . NIL . LISPAX . NIL . 5 .) ((→ GROUND TRUTHVAL) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 750) (UNARY& . LISTP)) . (#& . 11) . CONSTANT .) ((((∀ U)) NIL ((SYMBOL& NIL . SEXP) NIL (SYMBOL& NIL . U))) . (AXIOM (TM& ((∀ U)) NIL ((SYMBOL& NIL . SEXP) NIL (SYMBOL& NIL . U)))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 15 .) (GROUND . (SYMBOL& NIL . ATOM) . NIL . NIL . (#& . 6) . VARIABLE .) (GROUND . (SYMBOL& NIL . ATOM) . NIL . NIL . (#& . 6) . VARIABLE .) (NIL . (DECL (XA YA ZA) (TYPE: (TY& . GROUND)) (SORT: (TM& SYMBOL& NIL . ATOM))) . ((ZA #& . 5) (ATOM #& . 1) (YA #& . 7) (ATOM #& . 1) (XA #& . 8) (ATOM #& . 1)) . NIL . NIL . NIL . LISPAX . NIL . 10 .) (GROUND . (SYMBOL& NIL . ATOM) . NIL . NIL . (#& . 6) . VARIABLE .) (NIL . (DECL SEXP (UNARYNAME: SEXP) (TYPE: (TY& → GROUND TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((SEXP #& . 3)) . NIL . NIL . NIL . LISPAX . NIL . 7 .) ((→ GROUND TRUTHVAL) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 750) (UNARY& . SEXP)) . (#& . 4) . CONSTANT .) (NIL . (DECL ATOM (UNARYNAME: ATOM) (TYPE: (TY& → GROUND TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((ATOM #& . 1)) . NIL . NIL . NIL . LISPAX . NIL . 3 .) ((→ GROUND TRUTHVAL) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 750) (UNARY& . ATOM)) . (#& . 2) . CONSTANT .) ((((∀ XA)) NIL ((SYMBOL& NIL . SEXP) NIL (SYMBOL& NIL . XA))) . (AXIOM (TM& ((∀ XA)) NIL ((SYMBOL& NIL . SEXP) NIL (SYMBOL& NIL . XA)))) . ((ATOM #& . 1) (SEXP #& . 3) (ZA #& . 5) (YA #& . 7) (XA #& . 8)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 14 .))